Natural numbers as lambda terms.md (958B)
1 +++ 2 title = "Natural numbers as lambda terms" 3 +++ 4 5 # Natural numbers as lambda terms 6 ## Church numerals 7 Try to find infinitely many different closed normal forms that let us calculate. 8 9 <pre> 10 zero => z 11 successor(zero) => s z 12 successor(successor(zero)) => s (s z) 13 </pre> 14 15 ∴ infinite, many, different, normal. 16 17 <pre> 18 c0 = λs.λz.z 19 c1 = λs.λz.s(z) 20 c2 = λs.λz.s(s((z))) 21 ... 22 cn = λs.λz.sⁿ(z) 23 </pre> 24 25 ∴ closed. 26 27 how to find definition of successor? 28 29 <pre> 30 s cn =β cn + 1 31 (in english, successor of Church numeral n is the same as the Church numeral + 1) 32 33 c₁ = λsz.sz 34 c₂ = λsz.s (s z) 35 36 ∴ s = λx.λsz.x s (s z) 37 = λx.λsz.s (x s z) 38 </pre> 39 40 ## Definability 41 a function `f : N —> N` is definable in lambda calculus by term F if `F[n] =β [ f (n) ]` for every n in N 42 43 for Church numerals only: `F cn =β cf (n)` 44 45 You can define successor as: `S = λx.λsz.s(xsz)` OR `S' = λx.λsz.xs(sz)`